\begin{tabbing}
weak{-}precond{-}send{-}p(${\it es}$;$T$;$A$;$l$;${\it tg}$;$a$;${\it ds}$;$P$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. vartype(source($l$);$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)\+
\\[0ex]\& $\forall$$e$@source($l$). kind($e$) $=$ locl($a$) $\Rightarrow$ valtype($e$) $\subseteq\rho$ $A$
\\[0ex]\& ($\forall$$e$:E. kind($e$) $=$ rcv($l$,${\it tg}$) $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$)
\\[0ex]\& \=(\=$\forall$${\it e'}$:E.\+\+
\\[0ex]kind(${\it e'}$) $=$ rcv($l$,${\it tg}$)
\\[0ex]$\Rightarrow$ \=kind(sender(${\it e'}$)) $=$ locl($a$)\+
\\[0ex]\& \=$P$((state when sender(${\it e'}$)),val(sender(${\it e'}$)))\+
\\[0ex]\& val(${\it e'}$) $=$ $f$((state when sender(${\it e'}$)),val(sender(${\it e'}$))))
\-\-\-\\[0ex]\& \=$\forall$$e$@source($l$).\+
\\[0ex]$\exists$${\it e'}$:E.
\\[0ex]$e$ c$\leq$ ${\it e'}$
\\[0ex]\& \=kind(${\it e'}$) $=$ rcv($l$,${\it tg}$) \& $e$ $\leq$ sender(${\it e'}$) \+
\\[0ex]$\vee$ loc(${\it e'}$) $=$ source($l$) \& ($\forall$$v$:$A$. $\neg$$P$(state after ${\it e'}$,$v$))
\-\-\-\-
\end{tabbing}